/*
 * EscMissesBugAfterLoop.java
 * 
 * Copyright 2008 Christoph Csallner and Yannis Smaragdakis.
 */
package edu.gatech.cc.cnc.examples;

/**
 * @author csallner@gatech.edu (Christoph Csallner)
 */
public class EscMissesBugAfterLoop {

	/**
	 * ESC/Java misses this clear division by zero exception.
	 * 
	 * ``Therefore, ESC/Java approximates the semantics of loops by 
	 * unrolling them a fixed number of times and replacing the 
	 * remaining iterations by code that terminates without ever producing 
	 * an error. This misses errors that occur only in or after later
	 * iterations of a loop.''
	 * [Flanagan et al., ESC/Java paper, PLDI 2002]
	 */
	public int bugAfterLoop() {
		int i = 0;
		while (i<100)
			i++;
		
		return 1/0;
	}
}
